Nuprl Definition : trivial-component
11,40
postcript
pdf
trivial-component(
f
)(
X
) == <scheme-none(), interface-compose(
x
.inl (
f
(
x
)) ;
X
)>
latex
Definitions
<
a
,
b
>
,
scheme-none()
,
interface-compose(
f
;
X
)
,
x
.
A
(
x
)
,
inl
x
,
f
(
a
)
FDL editor aliases
trivial-component
origin
x.inl (f(x)) ;X)> x.inl (f(x)) ;X)> x.A(x)